import Mathlib.Algebra.Group.Defs import Mathlib.Init.Algebra.Order import ECTate.Algebra.Ring.Basic import Mathlib.Init.Data.Nat.Lemmas import ECTate.Init.Data.Int.Lemmas import ECTate.Data.Nat.Enat import ECTate.Algebra.EllipticCurve.Kronecker import Mathlib.Tactic.LibrarySearch import Mathlib.Tactic.Ring import Mathlib.Tactic.Convert --class ValueMonoid (A : Type u) extends AddCommMonoid A, LinearOrder A open Enat section Obvious lemmamatch_non_zero (x :x: ββͺβββͺβ) {ββͺβ: Typec1c1: Ξ²c2 :c2: Ξ²Ξ²} :Ξ²: ?m.5x βx: ββͺβ0 β (match0: ?m.18x with |x: ββͺβ0 =>0: ββͺβc1 | _ =>c1: Ξ²c2) =c2: Ξ²c2 :=c2: Ξ²Goals accomplished! πGoals accomplished! πtheorem nat_mul_left_cancel (Goals accomplished! πaa: βbb: βc :c: βNat) (Nat: Typeh :h: a β 0a βa: β0) :0: ?m.940a *a: βb =b: βa *a: βc βc: βb =b: βc := Nat.eq_of_mul_eq_mul_left (Nat.pos_of_ne_zeroc: βh) end Obvious structure SurjVal {h: a β 0R :R: Type uType u} (Type u: Type (u + 1)p :p: RR) [R: Type uIntegralDomainIntegralDomain: Type ?u.1068 β Type ?u.1068R] whereR: Type uv :v: {R : Type u} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβR βR: Type uββͺβββͺβ: Typev_uniformizer :v_uniformizer: β {R : Type u} {p : R} [inst : IntegralDomain R] (self : SurjVal p), SurjVal.v self p = ofN 1vv: R β ββͺβp = ofNp: R1 v_mul_eq_add_v (1: ?m.1079aa: Rb :b: RR) :R: Type uv (v: R β ββͺβa *a: Rb) =b: Rvv: R β ββͺβa +a: Rvv: R β ββͺβb v_add_ge_min_v (b: Raa: Rb :b: RR) :R: Type uv (v: R β ββͺβa +a: Rb) β₯b: Rmin (min: {Ξ± : Type ?u.1326} β [self : Min Ξ±] β Ξ± β Ξ± β Ξ±vv: R β ββͺβa) (a: Rvv: R β ββͺβb) v_eq_top_iff_zero (b: Ra :a: RR) :R: Type uvv: R β ββͺβa =a: Rβ ββ: ββͺβa =a: R0 variable {0: ?m.1352R :R: Type uType u} [Type u: Type (u + 1)IntegralDomainIntegralDomain: Type ?u.2226 β Type ?u.2226R] section SurjVal lemmaR: Type up_non_zero {p_non_zero: β {R : Type u} [inst : IntegralDomain R] {p : R}, SurjVal p β Β¬p = 0p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2061} β R β [inst : IntegralDomain R] β Type ?u.2061p) : Β¬p: Rp =p: R0 :=0: ?m.2071@[simp] lemmaGoals accomplished! πval_zero {val_zero: β {R : Type u} [inst : IntegralDomain R] {p : R} (nav : SurjVal p), SurjVal.v nav 0 = βp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2231} β R β [inst : IntegralDomain R] β Type ?u.2231p) :p: Rnav.nav: SurjVal pvv: {R : Type ?u.2240} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβ0 =0: ?m.2248β := (β: ββͺβnav.v_eq_top_iff_zeronav: SurjVal p0).0: ?m.230822: β {a b : Prop}, (a β b) β b β arfl lemma val_mul_ge_left {rfl: β {Ξ± : Sort ?u.2314} {a : Ξ±}, a = ap :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2340} β R β [inst : IntegralDomain R] β Type ?u.2340p) (p: Raa: Rb :b: RR) :R: Type unav.nav: SurjVal pv (v: {R : Type ?u.2353} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rnav.nav: SurjVal pvv: {R : Type ?u.2453} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa := Enat.le_trans (le_add_right (a: Rnav.nav: SurjVal pvv: {R : Type ?u.2478} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa) (a: Rnav.nav: SurjVal pvv: {R : Type ?u.2482} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb)) (le_of_eq (b: Rnav.v_mul_eq_add_vnav: SurjVal paa: Rb).symm) lemmab: Rval_mul_ge_right {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2522} β R β [inst : IntegralDomain R] β Type ?u.2522p) (p: Raa: Rb :b: RR) :R: Type unav.nav: SurjVal pv (v: {R : Type ?u.2535} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rnav.nav: SurjVal pvv: {R : Type ?u.2635} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb :=b: RlemmaGoals accomplished! πval_mul_ge_of_left_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2786} β R β [inst : IntegralDomain R] β Type ?u.2786p) {p: Raa: Rb :b: RR} (ha :R: Type unav.nav: SurjVal pvv: {R : Type ?u.2796} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rn) :n: ?m.2781nav.nav: SurjVal pv (v: {R : Type ?u.2808} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rn := Enat.le_trans ha (val_mul_ge_leftn: ?m.2781navnav: SurjVal paa: Rb) lemmab: Rval_mul_ge_of_right_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2976} β R β [inst : IntegralDomain R] β Type ?u.2976p) {p: Raa: Rb :b: RR} (hb :R: Type unav.nav: SurjVal pvv: {R : Type ?u.2986} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb β₯b: Rn) :n: ?m.2971nav.nav: SurjVal pv (v: {R : Type ?u.2998} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rn := Enat.le_trans hb (val_mul_ge_rightn: ?m.2971navnav: SurjVal paa: Rb) lemmab: Rval_mul_ge_of_both_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.3198} β R β [inst : IntegralDomain R] β Type ?u.3198p) {p: Raa: Rb :b: RR} (ha :R: Type unav.nav: SurjVal pvv: {R : Type ?u.3176} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rm) (hb :m: ?m.3161nav.nav: SurjVal pvv: {R : Type ?u.3217} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb β₯b: Rn) :n: ?m.3193nav.nav: SurjVal pv (v: {R : Type ?u.3226} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rm +m: ?m.3161n :=n: ?m.3193@[simp] lemma val_of_one {Goals accomplished! πp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.3442} β R β [inst : IntegralDomain R] β Type ?u.3442p) :p: Rnav.nav: SurjVal pvv: {R : Type ?u.3451} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβ1 = ofN1: ?m.34590 :=0: ?m.3511
alemmaGoals accomplished! πval_pow_ge_of_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.3745} β R β [inst : IntegralDomain R] β Type ?u.3745p) {p: Ra :a: RR} (R: Type uk :k: ββ) (ha :β: Typenav.nav: SurjVal pvv: {R : Type ?u.3755} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rm) :m: ?m.3740nav.nav: SurjVal pv (v: {R : Type ?u.3767} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa ^a: Rk) β₯k: βk β’k: βm :=m: ?m.3740Goals accomplished! πlemmaGoals accomplished! πval_add_ge_of_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.11142} β R β [inst : IntegralDomain R] β Type ?u.11142p) {p: Raa: Rb :b: RR} (ha :R: Type unav.nav: SurjVal pvv: {R : Type ?u.11152} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rn) (hb :n: ?m.11137nav.nav: SurjVal pvv: {R : Type ?u.11164} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb β₯b: Rn) :n: ?m.11137nav.nav: SurjVal pv (v: {R : Type ?u.11173} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa +a: Rb) β₯b: Rn := Enat.le_trans (n: ?m.11137le_min ha hb) (le_min: β {Ξ± : Type ?u.11298} [inst : LinearOrder Ξ±] {a b c : Ξ±}, c β€ a β c β€ b β c β€ min a bnav.v_add_ge_min_vnav: SurjVal paa: Rb) def nat_of_val {b: Rp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.11326} β R β [inst : IntegralDomain R] β Type ?u.11326p) {p: Ra :a: RR} (R: Type uh :h: a β 0a βa: R0) :0: ?m.11339β := to_nat ((not_iff_not.β: Type2 (2: β {a b : Prop}, (a β b) β b β anav.v_eq_top_iff_zeronav: SurjVal pa)).a: R22: β {a b : Prop}, (a β b) β b β ah) /- lemma val_of_add_one {p : R} (nav : SurjVal p) (h : nav.v x β₯ ofN 1): nav.v (x + 1) = ofN 0 := by apply Enat.le_antisymm . apply le_of_not_lt intro h' sorry . apply Enat.le_trans _ (nav.v_add_ge_min_v x 1) apply le_min (Enat.le_trans (Enat.le_succ 0) h) (le_of_eq (val_of_one nav).symm) -/ @[simp] lemmah: a β 0val_of_minus_one {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.11498} β R β [inst : IntegralDomain R] β Type ?u.11498p) :p: Rnav.nav: SurjVal pv (-v: {R : Type ?u.11507} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβ1) = ofN1: ?m.115160 :=0: ?m.11599Goals accomplished! πGoals accomplished! π@[simp] lemma val_neg {Goals accomplished! πp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.12163} β R β [inst : IntegralDomain R] β Type ?u.12163p) :p: Rnav.nav: SurjVal pv (-v: {R : Type ?u.12169} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx) =x: ?m.12158nav.nav: SurjVal pvv: {R : Type ?u.12197} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx :=x: ?m.12158lemmaGoals accomplished! πval_sub_ge_of_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.12467} β R β [inst : IntegralDomain R] β Type ?u.12467p) {p: Raa: Rb :b: RR} (ha :R: Type unav.nav: SurjVal pvv: {R : Type ?u.12477} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rn) (hb :n: ?m.12462nav.nav: SurjVal pvv: {R : Type ?u.12489} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb β₯b: Rn) :n: ?m.12462nav.nav: SurjVal pv (v: {R : Type ?u.12498} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa -a: Rb) β₯b: Rn :=n: ?m.12462theoremGoals accomplished! πv_add_eq_min_v {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.13017} β R β [inst : IntegralDomain R] β Type ?u.13017p) {p: Raa: Rb :b: RR} (h :R: Type unav.nav: SurjVal pvv: {R : Type ?u.13030} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa <a: Rnav.nav: SurjVal pvv: {R : Type ?u.13037} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb) :b: Rnav.nav: SurjVal pv (v: {R : Type ?u.13049} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa +a: Rb) =b: Rnav.nav: SurjVal pvv: {R : Type ?u.13150} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa :=a: RGoals accomplished! πGoals accomplished! πtheorem val_of_pow_uniformizer {Goals accomplished! πp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.13888} β R β [inst : IntegralDomain R] β Type ?u.13888p) :p: Rnav.nav: SurjVal pv (v: {R : Type ?u.13919} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβp ^p: Rn) = ofNn: ?m.13908n :=n: ?m.13908Goals accomplished! πend SurjVal structureGoals accomplished! πEnatValRing {EnatValRing: {R : Type u} β {p : R} β [inst : IntegralDomain R] β (valtn : SurjVal p) β (decr_val : R β R) β (β {x : R}, SurjVal.v valtn x = 0 β decr_val x = x) β (β {x : R}, SurjVal.v valtn x > 0 β x = p * decr_val x) β (residue_char : β) β (β (n : β), SurjVal.v valtn βn > 0 β residue_char β£ n) β (R β R) β (R β R β R β Bool) β EnatValRing pR :R: Type uType u} (Type u: Type (u + 1)p :p: RR) [R: Type uIntegralDomainIntegralDomain: Type ?u.14523 β Type ?u.14523R] whereR: Type uvaltn :valtn: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pSurjValSurjVal: {R : Type ?u.14528} β R β [inst : IntegralDomain R] β Type ?u.14528pp: Rdecr_val :decr_val: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β RR βR: Type uRR: Type uzero_valtn_decr {zero_valtn_decr: β {R : Type u} {p : R} [inst : IntegralDomain R] (self : EnatValRing p) {x : R}, SurjVal.v self.valtn x = 0 β EnatValRing.decr_val self x = xx :x: RR} (h :R: Type uvaltn.valtn: SurjVal pvv: {R : Type ?u.14543} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx =x: R0) :0: ?m.14551decr_valdecr_val: R β Rx =x: Rxx: Rpos_valtn_decr {pos_valtn_decr: β {R : Type u} {p : R} [inst : IntegralDomain R] (self : EnatValRing p) {x : R}, SurjVal.v self.valtn x > 0 β x = p * EnatValRing.decr_val self xx :x: RR} (h :R: Type uvaltn.valtn: SurjVal pvv: {R : Type ?u.14789} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx >x: R0) :0: ?m.14794x =x: Rp *p: Rdecr_valdecr_val: R β Rxx: Rresidue_char :residue_char: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β βββ: Typedef_char : βdef_char: β {R : Type u} {p : R} [inst : IntegralDomain R] (self : EnatValRing p) (n : β), SurjVal.v self.valtn βn > 0 β self.residue_char β£ nn :n: ββ,β: Typevaltn.valtn: SurjVal pv (v: {R : Type ?u.14919} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβn :n: βR) >R: Type u0 β0: ?m.15002residue_char β£residue_char: βnn: βnorm_repr :norm_repr: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β RR βR: Type uR --generalization of moduloR: Type uquad_roots_in_residue_field :quad_roots_in_residue_field: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β R β R β BoolR βR: Type uR βR: Type uR βR: Type uBool namespace EnatValRing /-- reduce the element x by valuation n (by dividing by an appropriate power of the uniformizer) -/ defBool: Typesub_val {sub_val: {p : R} β EnatValRing p β R β β β Rp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.16027} β R β [inst : IntegralDomain R] β Type ?u.16027p) (p: Rx :x: RR) (R: Type un :n: ββ) :β: TypeR := matchR: Type un with |n: β0 =>0: βx | Nat.succx: Rn => matchn: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.16069} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.16076} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx with |x: R0 =>0: ββͺβx | _ =>x: Rsub_valsub_val: {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing pevr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.16308} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx)x: Rn @[simp] lemman: βdecr_val_zero {decr_val_zero: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p), decr_val evr 0 = 0p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.16777} β R β [inst : IntegralDomain R] β Type ?u.16777p) :p: Revr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.16786} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β R0 =0: ?m.167940 :=0: ?m.16846
h
h
h
h
hGoals accomplished! π@[simp] lemmaGoals accomplished! πdecr_val_neg {decr_val_neg: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) (x : R), decr_val evr (-x) = -decr_val evr xp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.17150} β R β [inst : IntegralDomain R] β Type ?u.17150p) (p: Rx :x: RR) :R: Type uevr.evr: EnatValRing pdecr_val (-decr_val: {R : Type ?u.17161} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx) = -x: Revr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.17193} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx :=x: R
inl
inlGoals accomplished! π
inlGoals accomplished! π
inr
inrGoals accomplished! π
inr
inr@[simp] lemmaGoals accomplished! πdecr_val_p_mul {decr_val_p_mul: β {p : R} (evr : EnatValRing p) (x : R), decr_val evr (p * x) = xp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.17833} β R β [inst : IntegralDomain R] β Type ?u.17833p) (p: Rx :x: RR) :R: Type uevr.evr: EnatValRing pdecr_val (decr_val: {R : Type ?u.17844} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rp *p: Rx) =x: Rx :=x: RGoals accomplished! π@[simp] lemmaGoals accomplished! πsub_val_zero_n {sub_val_zero_n: β {p : R} (evr : EnatValRing p) (n : β), sub_val evr 0 n = 0p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.18284} β R β [inst : IntegralDomain R] β Type ?u.18284p) (p: Rn :n: ββ) :β: Typesub_valsub_val: {R : Type ?u.18295} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing p00: ?m.18306n =n: β0 :=0: ?m.18358
zeroGoals accomplished! π
succ@[simp] lemmaGoals accomplished! πsub_val_x_zero {sub_val_x_zero: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) (x : R), sub_val evr x 0 = xp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.19764} β R β [inst : IntegralDomain R] β Type ?u.19764p) (p: Rx :x: RR) :R: Type usub_valsub_val: {R : Type ?u.19775} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: R0 =0: ?m.19786x :=x: RlemmaGoals accomplished! πsub_val_val_zero {sub_val_val_zero: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) (x : R) (m : β), SurjVal.v evr.valtn x = 0 β sub_val evr x m = xp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.19845} β R β [inst : IntegralDomain R] β Type ?u.19845p) (p: Rx :x: RR) (R: Type um :m: ββ) (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.19858} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.19865} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx =x: R0) :0: ?m.19873sub_valsub_val: {R : Type ?u.20105} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rm =m: βx :=x: R
zeroGoals accomplished! π
succlemmaGoals accomplished! πsub_val_val_pos_succ {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.20733} β R β [inst : IntegralDomain R] β Type ?u.20733p) (p: Rx :x: RR) (R: Type um :m: ββ) (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.20747} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.20754} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx βx: R0) :0: ?m.20762sub_valsub_val: {R : Type ?u.20980} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing px (Nat.succx: Rm) =m: βsub_valsub_val: {R : Type ?u.20987} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing pevr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.20994} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx)x: Rm :=m: βlemmaGoals accomplished! πval_decr_val {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.22694} β R β [inst : IntegralDomain R] β Type ?u.22694p) (p: Rx :x: RR) (h :R: Type uevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.22702} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.22706} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx = ofNx: Rm) :m: ?m.22689evr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.22714} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv (v: {R : Type ?u.22718} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβevr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.22722} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx) = ofN (x: Rm -m: ?m.226891) :=1: ?m.22730R: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)R: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)R: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)lemmaGoals accomplished! πsub_val_decr_val_comm {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.23144} β R β [inst : IntegralDomain R] β Type ?u.23144p) (p: Rx :x: RR) (R: Type un :n: ββ) :β: Typesub_valsub_val: {R : Type ?u.23157} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing pevr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.23167} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx)x: Rn =n: βevr.evr: EnatValRing pdecr_val (decr_val: {R : Type ?u.23171} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rsub_valsub_val: {R : Type ?u.23175} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn) :=n: β
zeroGoals accomplished! πGoals accomplished! πGoals accomplished! πGoals accomplished! πlemmaGoals accomplished! πval_sub_val_eq {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.24086} β R β [inst : IntegralDomain R] β Type ?u.24086p) (p: Rx :x: RR) (R: Type un :n: ββ) (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.24096} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.24100} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx = ofNx: Rm) :m: ?m.24081evr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.24108} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv (v: {R : Type ?u.24112} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβsub_valsub_val: {R : Type ?u.24116} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn) = ofN (n: βm -m: ?m.24081n) :=n: β
zero
zeroGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hGoals accomplished! πlemmaGoals accomplished! πval_sub_val_le {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.24824} β R β [inst : IntegralDomain R] β Type ?u.24824p) (p: Rx :x: RR) (R: Type un :n: ββ) (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.24834} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.24838} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rm) :m: ?m.24819evr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.24850} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv (v: {R : Type ?u.24854} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβsub_valsub_val: {R : Type ?u.24858} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn) β₯ ofN (n: βm -m: ?m.24819n) :=n: βGoals accomplished! πGoals accomplished! πlemmaGoals accomplished! πfactor_p_of_le_val {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.25381} β R β [inst : IntegralDomain R] β Type ?u.25381p) {p: Rx :x: RR} {R: Type un :n: ββ} (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.25394} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.25401} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) :n: βx =x: Rp ^p: Rn *n: βsub_valsub_val: {R : Type ?u.25422} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn :=n: βR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
h: SurjVal.v evr.valtn x β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
h: SurjVal.v evr.valtn x β₯ ofN nGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
h: SurjVal.v evr.valtn x β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
pos_val: SurjVal.v evr.valtn (sub_val evr x n) > 0
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
pos_val: SurjVal.v evr.valtn (sub_val evr x n) > 0
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
pos_val: SurjVal.v evr.valtn (sub_val evr x n) > 0
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
pos_val: SurjVal.v evr.valtn (sub_val evr x n) > 0
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hlemmaGoals accomplished! πfactor_p_of_eq_val {factor_p_of_eq_val: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) {x : R} {n : β}, SurjVal.v evr.valtn x = ofN n β x = p ^ n * sub_val evr x np :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.26581} β R β [inst : IntegralDomain R] β Type ?u.26581p) {p: Rx :x: RR} {R: Type un :n: ββ} (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.26594} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.26601} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx = ofNx: Rn) :n: βx =x: Rp ^p: Rn *n: βsub_valsub_val: {R : Type ?u.26618} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn :=n: βfactor_p_of_le_valfactor_p_of_le_val: β {R : Type ?u.26838} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) {x : R} {n : β}, SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x nevr (le_of_eq (Eq.symm h)) lemma sub_val_p_mul {evr: EnatValRing pp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.26901} β R β [inst : IntegralDomain R] β Type ?u.26901p) (p: Rx :x: RR) (R: Type un :n: ββ) :β: Typesub_valsub_val: {R : Type ?u.26914} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing pp ^p: Rn *n: βx)x: Rn =n: βx :=x: R
zero
zero
zero
zero
zero
zero
zeroGoals accomplished! π
succ
succ.h
succ
succ.h
succ
succ.hlemmaGoals accomplished! πsub_val_neg {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.27819} β R β [inst : IntegralDomain R] β Type ?u.27819p) {p: Rx :x: RR} {R: Type un :n: ββ} :β: Typesub_valsub_val: {R : Type ?u.27832} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (-evr: EnatValRing px)x: Rn = -n: βsub_valsub_val: {R : Type ?u.27867} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn :=n: β
zeroGoals accomplished! πGoals accomplished! πGoals accomplished! πGoals accomplished! πlemmaGoals accomplished! πsub_val_add {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.28616} β R β [inst : IntegralDomain R] β Type ?u.28616p) {p: Rxx: Ry :y: RR} {R: Type un :n: ββ} (hx :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.28631} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.28638} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) (hy :n: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.28653} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.28657} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rn) :n: βsub_valsub_val: {R : Type ?u.28666} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px +x: Ry)y: Rn =n: βsub_valsub_val: {R : Type ?u.28773} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn +n: βsub_valsub_val: {R : Type ?u.28780} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rn :=n: βR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nlemmaGoals accomplished! πsub_val_sub {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.29284} β R β [inst : IntegralDomain R] β Type ?u.29284p) {p: Rxx: Ry :y: RR} {R: Type un :n: ββ} (hx :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.29299} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.29306} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) (hy :n: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.29321} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.29325} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rn) :n: βsub_valsub_val: {R : Type ?u.29334} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px -x: Ry)y: Rn =n: βsub_valsub_val: {R : Type ?u.29405} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn -n: βsub_valsub_val: {R : Type ?u.29412} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rn :=n: βR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nlemmaGoals accomplished! πsub_val_mul_left {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.29977} β R β [inst : IntegralDomain R] β Type ?u.29977p) {p: Rxx: Ry :y: RR} {R: Type un :n: ββ} (hx :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.29992} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.29999} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) :n: βsub_valsub_val: {R : Type ?u.30014} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px *x: Ry)y: Rn =n: βsub_valsub_val: {R : Type ?u.30117} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn *n: βy :=y: RR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
aGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN nlemmaGoals accomplished! πsub_val_mul_right {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.30621} β R β [inst : IntegralDomain R] β Type ?u.30621p) {p: Rxx: Ry :y: RR} {R: Type un :n: ββ} (hy :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.30636} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.30643} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rn) :n: βsub_valsub_val: {R : Type ?u.30658} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px *x: Ry)y: Rn =n: βx *x: Rsub_valsub_val: {R : Type ?u.30761} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rn :=n: βlemmaGoals accomplished! πsub_val_mul_sub_val {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.30944} β R β [inst : IntegralDomain R] β Type ?u.30944p) {p: Rxx: Ry :y: RR} (R: Type unn: βm :m: ββ) (hx :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.30961} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.30968} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) (hy :n: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.30983} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.30987} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rm) :m: βsub_valsub_val: {R : Type ?u.30999} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn *n: βsub_valsub_val: {R : Type ?u.31006} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rm =m: βsub_valsub_val: {R : Type ?u.31013} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px *x: Ry) (y: Rn +n: βm) :=m: βR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mGoals accomplished! πlemmaGoals accomplished! πsub_val_mul {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.32226} β R β [inst : IntegralDomain R] β Type ?u.32226p) {p: Rxx: Ry :y: RR} (R: Type unn: βm :m: ββ) {β: Typenm :nm: ββ} (h :β: Typen +n: βm =m: βnm) (hx :nm: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.32289} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.32296} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) (hy :n: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.32311} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.32315} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rm) :m: βsub_valsub_val: {R : Type ?u.32324} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px *x: Ry)y: Rnm =nm: βsub_valsub_val: {R : Type ?u.32427} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn *n: βsub_valsub_val: {R : Type ?u.32434} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rm :=m: βlemmaGoals accomplished! πsub_val_pow {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.32563} β R β [inst : IntegralDomain R] β Type ?u.32563p) {p: Rx :x: RR} (R: Type unn: βk :k: ββ) {β: Typenm :nm: ββ} (h :β: Typek *k: βn =n: βnm) (hx :nm: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.32628} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.32635} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) :n: βsub_valsub_val: {R : Type ?u.32650} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px ^x: Rk)k: βnm =nm: βsub_valsub_val: {R : Type ?u.32790} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn ^n: βk :=k: βGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nmR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hylemmaGoals accomplished! πsub_val_sub_val {sub_val_sub_val: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) {x : R} {m n : β}, sub_val evr (sub_val evr x m) n = sub_val evr x (m + n)p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.33685} β R β [inst : IntegralDomain R] β Type ?u.33685p) {p: Rx :x: RR} {R: Type umm: βn :n: ββ} :β: Typesub_valsub_val: {R : Type ?u.33700} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing psub_valsub_val: {R : Type ?u.33710} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rm)m: βn =n: βsub_valsub_val: {R : Type ?u.33714} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing px (x: Rm +m: βn) :=n: β
zeroGoals accomplished! πGoals accomplished! πGoals accomplished! πdefGoals accomplished! πhas_double_root {has_double_root: {p : R} β (evr : EnatValRing p) β (a b c : R) β ?m.34400 evr a b cp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.34385} β R β [inst : IntegralDomain R] β Type ?u.34385p) (p: Raa: Rbb: Rc :c: RR) :=R: Type uevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.34421} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.34425} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa =a: R0 β§0: ?m.34433evr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.34663} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv (v: {R : Type ?u.34667} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb ^b: R2 -2: ?m.346784 *4: ?m.34694a *a: Rc) >c: R0 end EnatValRing def0: ?m.35007nat_prime (nat_prime: β β Propp :p: ββ) :β: TypeProp :=Prop: Type1 <1: ?m.35302p β§ (βp: βaa: βb :b: ββ, (β: Typea *a: βb) %b: βp =p: β0 β0: ?m.35349a %a: βp =p: β0 β¨0: ?m.35447b %b: βp =p: β0) lemma ndiv_mul_left (0: ?m.35486aa: βbb: βp :p: ββ) : (β: Typea *a: βb) %b: βp βp: β0 β0: ?m.35625a %a: βp βp: β0 :=0: ?m.35660lemma ndiv_mul_right (Goals accomplished! πaa: βbb: βp :p: ββ) : (β: Typea *a: βb) %b: βp βp: β0 β0: ?m.35924b %b: βp βp: β0 :=0: ?m.35959lemmaGoals accomplished! πnat_prime_test (p :p: ββ) :β: Typenat_primenat_prime: β β Propp β (p: β1 <1: ?m.36012p β§ (βp: βaa: βb :b: ββ,β: Typea <a: βp βp: βb <b: βp β (p: βa *a: βb) %b: βp =p: β0 β0: ?m.36069a %a: βp =p: β0 β¨0: ?m.36167b %b: βp =p: β0)) :=0: ?m.36206
mp
mpr
mp
mpr
mp
mpr
mp
mpr
mp
mprGoals accomplished! π:Goals accomplished! πDecidablePred (DecidablePred: {Ξ± : Sort ?u.36532} β (Ξ± β Prop) β Sort (max 1 ?u.36532)nat_prime . :nat_prime: β β Propβ ββ: TypeProp) := funProp: Typep =>p: ?m.36546sorry --match p with --| 0 => sorry --isFalse (not_and_of_not_left _ (not_lt_of_ge (le_of_lt Nat.zero_lt_one))) --| 1 => isFalse (not_and_of_not_left _ (not_lt_of_ge (le_of_eq rfl))) --| Nat.succ (Nat.succ p') => sorry --def fmul_eq_addf {R R' : Type u} [Mul R] [Add R'] (f : R β R') (x y : R) : Prop := f (x * y) = f x + f y namespace Int def nat_valuation :sorry: ?m.36549β ββ: Typeβ ββ: Typeββͺβ | _,ββͺβ: Type0 =>0: ββ |β: ββͺβ0, (0: β_+1) => ofN_: β0 |0: ?m.367001, (1: β_+1) =>_: ββ | (β: ββͺβq+2), (q: βm+1) => if (m: βm+m: β1) % (1: ?m.36881q+q: β2) β2: ?m.368950 then ofN0: ?m.369870 else succ (nat_valuation (0: ?m.36994q+q: β2) ((2: ?m.37000m+m: β1) / (1: ?m.37045q+q: β2))) termination_by nat_valuation p k =>2: ?m.37059k decreasing_byk: βlemmaGoals accomplished! πnat_val_zero (nat_val_zero: β (p : β), nat_valuation p 0 = βp :p: ββ) : nat_valuationβ: Typepp: β0 =0: ?m.38639β :=β: ββͺβnat_valuation p 0 = βlemmaGoals accomplished! πnat_val_succ (qq: βm :m: ββ) : nat_valuation (β: Typeq+q: β2) (2: ?m.51833m+m: β1) = if (1: ?m.51887m+m: β1) % (1: ?m.51948q+q: β2) β2: ?m.519620 then ofN0: ?m.520540 else succ (nat_valuation (0: ?m.52065q+q: β2) ((2: ?m.52071m+m: β1) / (1: ?m.52116q+q: β2))) :=2: ?m.52130def int_val (Goals accomplished! πp :p: ββ) (β: Typek :k: β€β€) :β€: Typeββͺβ := nat_valuationββͺβ: Typep (natAbsp: βk) lemma int_val_uniformizer {k: β€p :p: ββ} (β: Typegt1 :gt1: 1 < p1 <1: ?m.55151p) : int_valp: βpp: βp = ofNp: β1 :=1: ?m.55273nat_valuation p p = ofN 1nat_valuation p p = ofN 1nat_valuation 0 0 = ofN 1nat_valuation p p = ofN 1
hnat_valuation 0 0 = ofN 1
h1 < 0nat_valuation 0 0 = ofN 1Goals accomplished! πnat_valuation p p = ofN 1nat_valuation (Nat.succ 0) (Nat.succ 0) = ofN 1nat_valuation p p = ofN 1
hnat_valuation (Nat.succ 0) (Nat.succ 0) = ofN 1
h1 < 1nat_valuation (Nat.succ 0) (Nat.succ 0) = ofN 1Goals accomplished! πnat_valuation p p = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation p p = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1
hc
hcnat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1lemmaGoals accomplished! πnat_val_mul_eq_add (nat_val_mul_eq_add: β (p : β), nat_prime p β β (a b : β), nat_valuation p (a * b) = nat_valuation p a + nat_valuation p bp :p: ββ) (β: Typeprime :prime: nat_prime pnat_primenat_prime: β β Propp) (p: βaa: βb :b: ββ) : nat_valuationβ: Typep (p: βa *a: βb) = nat_valuationb: βpp: βa + nat_valuationa: βpp: βb :=b: βnat_valuation p (a * b) = nat_valuation p a + nat_valuation p bnat_valuation p (a * b) = nat_valuation p a + nat_valuation p bβ (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dβ (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeroβ (c d : β), c + d β€ Nat.zero β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeronat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeroβ (c d : β), c + d β€ Nat.zero β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeronat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeronat_valuation p (0 * d) = nat_valuation p 0 + nat_valuation p d
zeronat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeronat_valuation p (0 * 0) = nat_valuation p 0 + nat_valuation p 0
zeronat_valuation p (0 * 0) = nat_valuation p 0 + nat_valuation p 0
zeroβ (c d : β), c + d β€ Nat.zero β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dGoals accomplished! πβ (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
succβ (c d : β), c + d β€ Nat.succ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: c + d β€ Nat.succ n
succnat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
succβ (c d : β), c + d β€ Nat.succ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: c + d β€ Nat.succ n
succnat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
d: β
h_sum: Nat.zero + d β€ Nat.succ n
succ.zeronat_valuation p (Nat.zero * d) = nat_valuation p Nat.zero + nat_valuation p dGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: c + d β€ Nat.succ n
succnat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
d, c: β
h_sum: Nat.succ c + d β€ Nat.succ n
succ.succnat_valuation p (Nat.succ c * d) = nat_valuation p (Nat.succ c) + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
d, c: β
h_sum: Nat.succ c + d β€ Nat.succ n
succ.succnat_valuation p (Nat.succ c * d) = nat_valuation p (Nat.succ c) + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c: β
h_sum: Nat.succ c + Nat.zero β€ Nat.succ n
succ.succ.zeronat_valuation p (Nat.succ c * Nat.zero) = nat_valuation p (Nat.succ c) + nat_valuation p Nat.zeroGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
d, c: β
h_sum: Nat.succ c + d β€ Nat.succ n
succ.succnat_valuation p (Nat.succ c * d) = nat_valuation p (Nat.succ c) + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
succ.succ.succnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
succ.succ.succnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
succ.succ.succnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: 2 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p(if (c * d + c + d + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((c * d + c + d + 1) / (q + 2)))) = (if (c + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((c + 1) / (q + 2)))) + if (d + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((d + 1) / (q + 2)))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p(if (c * d + c + d + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((c * d + c + d + 1) / (q + 2)))) = (if (c + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((c + 1) / (q + 2)))) + if (d + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((d + 1) / (q + 2)))Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
xβ: (c + 1) * (d + 1) % p = 0 β¨ (c + 1) * (d + 1) % p > 0R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
xβ: (c + 1) % p = 0 β¨ (d + 1) % p = 0
inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p)) + nat_valuation p (d + 1)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p) + nat_valuation p (d + 1))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p) + nat_valuation p (d + 1))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p) + nat_valuation p (d + 1))Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p) + nat_valuation p (d + 1))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
inl.inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
inl.inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
inl.inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
mul_div_assoc: (c + 1) * (d + 1) / p = (c + 1) / p * (d + 1)
inl.inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
mul_div_assoc: (c + 1) * (d + 1) / p = (c + 1) / p * (d + 1)
inl.inlGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
xβ: (c + 1) % p = 0 β¨ (d + 1) % p = 0
inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = nat_valuation p (c + 1) + succ (nat_valuation p ((d + 1) / p))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p (c + 1) + nat_valuation p ((d + 1) / p))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p (c + 1) + nat_valuation p ((d + 1) / p))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p (c + 1) + nat_valuation p ((d + 1) / p))Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p (c + 1) + nat_valuation p ((d + 1) / p))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
inl.inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
inl.inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
inl.inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
mul_div_assoc: (c + 1) * (d + 1) / p = (c + 1) * ((d + 1) / p)
inl.inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
mul_div_assoc: (c + 1) * (d + 1) / p = (c + 1) * ((d + 1) / p)
inl.inrGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
xβ: (c + 1) * (d + 1) % p = 0 β¨ (c + 1) * (d + 1) % p > 0R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrGoals accomplished! πnat_valuation p (a * b) = nat_valuation p a + nat_valuation p blemmaGoals accomplished! πint_val_mul_eq_add (p :p: ββ) (β: Typeprime :prime: nat_prime pnat_primenat_prime: β β Propp) (p: βaa: β€b :b: β€β€) : int_valβ€: Typep (p: βa *a: β€b) = int_valb: β€pp: βa + int_vala: β€pp: βb :=b: β€nat_valuation p (natAbs a * natAbs b) = nat_valuation p (natAbs a) + nat_valuation p (natAbs b)lemma (Goals accomplished! πpp: βaa: βb :b: ββ) : nat_valuationβ: Typep (p: βa +a: βb) β₯b: βmin (nat_valuationmin: {Ξ± : Type ?u.60773} β [self : Min Ξ±] β Ξ± β Ξ± β Ξ±pp: βa) (nat_valuationa: βpp: βb) :=b: βnat_valuation p (a + b) β₯ min (nat_valuation p a) (nat_valuation p b)lemma (Goals accomplished! πaa: β€b :b: β€β€) : natAbs (β€: Typea +a: β€b) =b: β€max (natAbsmax: {Ξ± : Type ?u.60858} β [self : Max Ξ±] β Ξ± β Ξ± β Ξ±a) (natAbsa: β€b) -b: β€min (natAbsmin: {Ξ± : Type ?u.60864} β [self : Min Ξ±] β Ξ± β Ξ± β Ξ±a) (natAbsa: β€b) :=b: β€lemma (Goals accomplished! πp :p: ββ) (β: Typeaa: β€b :b: β€β€) : int_valβ€: Typep (p: βa +a: β€b) β₯b: β€min (int_valmin: {Ξ± : Type ?u.60970} β [self : Min Ξ±] β Ξ± β Ξ± β Ξ±pp: βa) (int_vala: β€pp: βb) :=b: β€nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b)) β₯ min (nat_valuation p (natAbs a)) (nat_valuation p (natAbs b))lemma (Goals accomplished! πp :p: ββ) (β: Typeaa: β€b :b: β€β€) (h : int_valβ€: Typepp: βa < int_vala: β€pp: βb) : int_valb: β€p (p: βa +a: β€b) = int_valb: β€pp: βa :=a: β€lemma (Goals accomplished! πp :p: ββ) (β: Typegt1 :gt1: 1 < p1 <1: ?m.61312p) (p: βa :a: β€β€) : int_valβ€: Typepp: βa =a: β€β ββ: ββͺβa =a: β€0 :=0: ?m.61353def primeVal {Goals accomplished! πp :p: ββ} (β: Typehp :hp: nat_prime pnat_primenat_prime: β β Propp) :p: βSurjVal (ofNatSurjVal: {R : Type ?u.61394} β R β [inst : IntegralDomain R] β Type ?u.61394p) := { v := int_valp: βp, v_uniformizer := int_val_uniformizerp: βhp.hp: nat_prime pleft, v_mul_eq_add_v := int_val_mul_eq_addleft: β {a b : Prop}, a β§ b β app: βhp, v_add_ge_min_v := int_val_add_ge_minhp: nat_prime pp, v_eq_top_iff_zero := int_val_eq_top_iff_zerop: βpp: βhp.hp: nat_prime pleft } def decr_val_p (left: β {a b : Prop}, a β§ b β ap :p: ββ) (val :β: Typeβ€ ββ€: Typeββͺβ) (ββͺβ: Typek :k: β€β€) :β€: Typeβ€ := match valβ€: Typek with |k: β€0 =>0: ββͺβk | _ =>k: β€k /k: β€p lemmap: βzero_valtn_decr_p {p:p: ββ} {β: Typek :k: β€β€} (val :β€: Typeβ€ ββ€: Typeββͺβ) (ββͺβ: Typeh : valh: val k = 0k =k: β€0) : decr_val_p0: ?m.62195p valp: βk =k: β€k :=k: β€decr_val_p p val k = kdecr_val_p p val k = kdecr_val_p p val k = kdef norm_repr_p (Goals accomplished! πp :p: ββ) (β: Typex :x: β€β€) :β€: Typeβ€ := (β€: Typex % (x: β€p :p: ββ€) +β€: Typep) % (p: βp :p: ββ€) lemma (β€: Typep :p: ββ) : ββ: Typen :n: ββ, (primeValβ: Typehp).hp: ?m.62796vv: {R : Type ?u.62808} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβn >n: β0 β0: ?m.62904p β£p: βn :=n: βsorry def {sorry: ?m.63136p :p: ββ} (β: Typehp :hp: nat_prime pnat_primenat_prime: β β Propp) :p: βEnatValRing (EnatValRing: {R : Type ?u.63153} β R β [inst : IntegralDomain R] β Type ?u.63153p :p: ββ€) := { valtn := primeValβ€: Typehp, decr_val := decr_val_php: nat_prime pp (primeValp: βhp).hp: nat_prime pv, zero_valtn_decr := zero_valtn_decr_p (primeValv: {R : Type ?u.63264} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβhp).hp: nat_prime pv, pos_valtn_decr :=v: {R : Type ?u.63278} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβsorry, residue_char :=sorry: ?m.63305p, def_char := def_char_pp: βp, norm_repr := norm_repr_pp: βp, quad_roots_in_residue_field := funp: βaa: ?m.64430bb: ?m.64433c => Int.quad_root_in_ZpZc: ?m.64436aa: ?m.64430bb: ?m.64433cc: ?m.64436p } lemma :p: βnat_primenat_prime: β β Prop2 :=2: ?m.64685lemma :Goals accomplished! πnat_primenat_prime: β β Prop3 :=3: ?m.64895def modulo (Goals accomplished! πx :x: β€β€) (β€: Typep :p: ββ) := (β: Typex % (x: β€p:p: ββ€) +β€: Typep) % (p: βp:p: ββ€) def inv_mod (β€: Typex :x: β€β€) (β€: Typep :p: ββ) := modulo (β: Typex ^ (x: β€p -p: β2))2: ?m.65427p def has_double_root (p: βaa: β€bb: β€c :c: β€β€) {β€: Typep :p: ββ} (β: Typehp :hp: nat_prime pnat_primenat_prime: β β Propp) := letp: βv_p := (v_p: ?m.65705primeEVRprimeEVR: {p : β} β nat_prime p β EnatValRing βphp).hp: nat_prime pvaltn.valtn: {R : Type ?u.65708} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv;v: {R : Type ?u.65718} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβv_pv_p: ?m.65705a =a: β€0 β§0: ?m.65741v_p (v_p: ?m.65705b ^b: β€2 -2: ?m.659774 *4: ?m.65993a *a: β€c) >c: β€0 def double_root (0: ?m.66214aa: β€bb: β€c :c: β€β€) (β€: Typep :p: ββ) := ifβ: Typep =p: β2 then modulo2: ?m.66492cc: β€2 else modulo (-2: ?m.66526b * inv_mod (b: β€2 *2: ?m.66536a)a: β€p)p: βp lemma {p: βp :p: ββ} (β: Typehp :hp: nat_prime pnat_primenat_prime: β β Propp) (p: βaa: β€bb: β€c :c: β€β€) (β€: TypeH : has_double_rootH: has_double_root a b c hpaa: β€bb: β€cc: β€hp) : lethp: nat_prime px := double_rootx: ?m.66755aa: β€bb: β€cc: β€p; letp: βv_p := (v_p: ?m.66758primeEVRprimeEVR: {p : β} β nat_prime p β EnatValRing βphp).hp: nat_prime pvaltn.valtn: {R : Type ?u.66760} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv;v: {R : Type ?u.66770} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβv_p (v_p: ?m.66758a*a: β€x^x: ?m.667552 +2: ?m.66795b*b: β€x +x: ?m.66755c) >c: β€0 β§0: ?m.67022v_p (v_p: ?m.667582*2: ?m.67334a*a: β€x +x: ?m.66755b) >b: β€0 :=0: ?m.67418end IntGoals accomplished! π